Section: New Results

Validation and Automation

Participants : Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Jingyan Jourdan-Lu, Mioara Joldeş, Vincent Lefèvre, Nicolas Louvet, Christophe Mouilleron, Hong Diep Nguyen, David Pfannholzer, Nathalie Revol, Philippe Théveny, Gilles Villard.

Efficient Implementation of Algorithms for Interval Linear Algebra

H.-D. Nguyen and N. Revol proposed an algorithm to solve linear systems with interval coefficients. The same approach can be used to verify the solution of a linear system with floating-point coefficients, i.e. to compute an interval enclosing the error between the exact solution and an approximate solution. The goal is twofold: on the one hand the accuracy of the solution is desired up to the last bit of the floating-point solution, on the other hand the efficiency of the implementation is obtained through the use of optimized BLAS3 routines [48] . The PhD thesis of H.-D. Nguyen [13] contains in particular the algorithm [24] and its properties. Its complexity has been established [47] and its potential use for symbolic-numeric computations has been discussed [50] .

Standardization of Interval Arithmetic

We contributed to the creation, and now chair, the IEEE 1788 working group on the standardization of interval arithmetic http://grouper.ieee.org/groups/1788/ . The main discussion topics of this working group [49] , for the year 2011, were exception handling (via decorations). An emerging topic is the repeatibility and reproducibility of interval computations. on the same platform or across different platforms.

Formal Proofs of the Arithmetic on Polynomial Models

Using as starting point [9] , the calculus with polynomial models, such as Taylor models, based on floating-point coefficients and floating-point operations, has been formalized and checked in Coq [18] . This calculus is at the core of Ariadne, an environment for the study of hybrid systems: the idea is to prove the environment itself, instead of using model-checking on the systems.

Formal Proof Generation for Elementary functions

The proof of the correct rounding property for an elementary function requires tight bounds on the error involved in the function code. F. de Dinechin, with Ch. Lauter (LIP6) and G. Melquiond (INRIA Proval) have described the use of the Gappa proof assistant to compute such tight bounds rigorously [27] .

Code Generation for Polynomial Evaluation

A given arithmetic expression may be evaluated on a computer in several ways, depending on the parenthesization and the ordering of terms in use. Among all the possible evaluations, one may want to choose one that is as fast and accurate as possible. In [12] Ch. Mouilleron introduced a set of algorithms in order to generate all these possible evaluations, to count them, and to find an optimal or nearly optimal one according to a given criteria. Thanks to this work, several sequences related to numbers of evaluations have been discovered and added to Sloane's on-line encyclopedia of integer sequences (OEIS). Moreover, this allowed to show experimentally that an algorithm by Paterson and Stockmeyer for the evaluation of a polynomial $p$ at a matrix point is optimal for small degrees of $p$. Finally, this work has led to the revamping of the software tool CGPE presented in [38] (see also § 5.5 ).